A, C:Type, eqa:EqDecider(A), eqc:EqDecider(C), eqc':Top, r:(AC), f:a:A fp Top, a:A.
{(a  dom(f))  (r(a)  dom(rename(r;f)))} 

latex

Definitions	{T}, t  T, x:A. B(x), EqDecider(T), Top, x. t(x), a:A fp B(a), b, P  Q, x  dom(f), rename(r;f), False, (x  l), , P  Q, map(f;as), deq-member(eq;x;L), eqof(d), p q, P  Q, P & Q, P  Q, x:A. B(x)
Lemmas	member map, iff transitivity, assert of bor, assert-deq-member, implies functionality wrt iff, or functionality wrt iff, deq property, bor wf, eqof wf, deq-member wf, map wf, assert wf, l member wf, member wf, false wf, fpf wf, top wf, deq wf